TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

Strict Trs:
  { if(true(), t, e) -> t
  , if(false(), t, e) -> e
  , member(x, []()) -> false()
  , member(x, ::(y, ys)) -> if(eq(x, y), true(), member(x, ys))
  , eq([](), []()) -> true()
  , eq(O(x), O(y)) -> eq(x, y)
  , eq(O(x), 1(y)) -> false()
  , eq(1(x), O(y)) -> false()
  , eq(1(x), 1(y)) -> eq(x, y)
  , negate(1(x)) -> 0(x)
  , negate(0(x)) -> 1(x)
  , choice(::(x, xs)) -> x
  , choice(::(x, xs)) -> choice(xs)
  , guess([]()) -> []()
  , guess(::(clause, cnf)) -> ::(choice(clause), guess(cnf))
  , verify([]()) -> true()
  , verify(::(l, ls)) ->
    if(member(negate(l), ls), false(), verify(ls))
  , sat(cnf) -> satck(cnf, guess(cnf))
  , satck(cnf, assign) -> if(verify(assign), assign, unsat()) }
Obligation:
  runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 300.0 seconds.

Arrrr..